COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		The object of this chapter is to explain some techniques for
C00012 00003	Extended lists and S-expressions.
C00015 ENDMK
C⊗;
	The object of this chapter is to explain some techniques for
proving that a LISP programs has desired properties.  Before
presenting them formally, we shall informally consider some
examples.
The familiar program for %2append%1ing two lists is given by

	%2u*v ← qif qn u qthen v qelse qa u . [qd u * v]%1.

We might like to prove that for any lists ⊗u and ⊗v, the program
terminates and that the function ⊗u*v has the following properties:

	%2qnil*u = u,

	u*qnil = u%1,

and

	%2u*[v*w] = [u*v]*w%1.

The first two statements express the fact is that qnil is the "zero" of
the append operation.
The standard mathematical terminology is to say that qnil is both a left
identity and a right identity for ⊗append.  The last equation
expresses the fact that
⊗append is associative - like addition and multiplication of numbers.
[Unlike addition and multiplication of numbers, ⊗append is not
commutative, since (A B)*(C D) = (A B C D) ≠ (C D)*(A B)].
Associativity allows us to write ⊗u*v*w, because it doesn't matter
how the expression is parenthesized.

	We postpone the question of whether the program always terminates,
because it involves new ideas.  For now we shall assume
that it does always terminate, and we rewrite the program as the equation

	%2u*v = qif qn u qthen v qelse qa u . [qd u * v]%1.

All we have done is to replace the ← sign by =, and we will assume that
the equation holds for all lists (lists not S-expressions) ⊗u and ⊗v. 

	Proving %2qnil*u = u%1, i.e. that qnil is a left identity
for ⊗append, is rather trivial.  We just substitute
in ({eq a5}) and get

	%2qnil*u = qif qn qnil qthen u qelse qa qnil . [qd qnil * u]

		= u%1.

That was too trivial, because we won't often succeed in proving what
we want just by substituting in function definitions and using known
properties of the elementary LISP functions.  In fact, when we want
to prove something about a function defined by recursion, we almost
always have to use some technique of mathematical induction in making
the proof.  Proving that qnil is a right identity requires such an
induction.  As before, we begin by substituting into ({eq a5}), but
this time we get

	%2u*qnil = qif qn u qthen qnil qelse qa u . [qd u * qnil]%1,

and this time the conditional expression does not just collapse.
However, notice that if ⊗u were qnil, ({eq a8}) would follow.  Notice
also that if ⊗u were not qnil, but
we knew that qnil was a right identity element for 
%2qd u%1, we could make the calculation

	u*qnil	= qa u . [qd u * qnil]

		= qa u . qd u

		= u,

and this is the what we want to prove.

	The induction technique for proving some proposition for all
⊗u is to prove it under the assumption that it holds for all
"smaller" ⊗u.  We then conclude that it holds for all ⊗u.
In this case, we are calling a list ⊗w1 "smaller"
than a list ⊗w2 if it is a "tail" of ⊗w2.

	The correctness of such an induction technique depends on the
notion of "smaller" satisfying what mathematicians call a "descending
chain condition".  Namely, given an element ⊗u, there must not be
an infinite descending chain of elements starting with ⊗u and each
smaller than the preceding.  In the case of lists, this is informally
obvious; if you keep taking sublists, you will eventually arrive at
the null list.

	A descending chain condition is all we need to make induction
work, because if a proposition concerning ⊗u follows from the same
proposition for all smaller elements, then the converse of the same
argument would derive from any counter example a smaller counter
example and hence an infinite descending chain of counter examples.
If there can't be any infinite descending chains at all, then there
can't be an infinite descending chain of counter examples.

	In the above argument, we have avoided mathematical symbolism.
In order to make the method easy to apply, we shall express all this
formally in the following sections.

	Before proceeding with the formalism, we remark that
associativity of ⊗u*v is proved by exactly the same kind of
inductive argument.  Only the algebra is a little more
complicated.  The induction hypothesis is that
⊗append is associative for all "smaller" ⊗u. 
Then there are two cases.

	If ⊗u is qnil, the theorem is an obvious consequence of the
fact that qnil is a left identity, i.e. the first theorem we proved.
If ⊗u is not qnil, we have

	[u*v]*w = [qa u . [qd u * v]] * w, using the definition of u*v,

		= qa [qa u . [qd u * v]] . [[qd [qa u . [qd u * v]] * w], using
			the definition of ⊗append to expand
			the second * of the previous line together with
			the fact that %2[qa u . [qd u * v]] cannot be qnil,
			since it is formed by a ⊗cons,

		= qa u . [[qd u * v] * w]%1, simplifying the above using
facts about qa and qd applied to [qa u . [qd u * v]],

		= qa u . [qd u * [v * w]]%1, using the induction hypothesis
			and the fact that %2qd u%1 is smaller than ⊗u. 

		= u * [v * w]%1, using the definition of ⊗append applied
			to the first * in %2u*[v*w]%1, i.e. going backwards.

	The algebra of this proof is rather typical.  We used the definition
of the function involved several times, we used the induction hypothesis
once, and we used the elementary algebraic facts about conditional
expressions and the basic functions of LISP.

Exercise:

	Consider ⊗reverse defined by

	%2reverse u ← rev1[u,qnil]%1

where

	%2rev1[u,v] ← qif qn u qthen v qelse rev1[qd u, qa u . v]%1.

Assume that the computation terminates for all lists ⊗u and ⊗v, so that
we may again replace ← by an =.  Prove that

	%2reverse[u*v] = reverse u * reverse v%1

and

	%2reverse reverse u = u%1.

The proof requires inventing suitable sentences on which to do the
inductions.
Extended lists and S-expressions.

	We now face the problem of what to do about the fact that
LISP programs cannot be assumed to always terminate.
That a program does terminate is often a big part of what we want to prove
about it.  Informally, we can proceed as we did in the previous section.
If we want to prove that ⊗u*v terminates, we assume that it terminates
for all "smaller" ⊗u and for all ⊗v.  Since the recursive definition
expresses ⊗u*v in terms of %2qd u * v]%1, this induction hypothesis
is sufficient to prove that it terminates for the given ⊗u. 

	The above argument is correct but informal.  We want to introduce
a formal notation so that we can prove termination by explicit rules
and eventually check the proofs by computer.  It turns out that we will be
able to replace
← by = even when the program may not terminate and
calculate with the resulting equation.  However, this requires extending
the range and domain of our functions by adjoining a new element
called qb (read "bottom").  When function doesn't terminate for
certain arguments, we
will give it the value qb.  Since the values of functions serve as
arguments to other functions, we must also say what elementary functions
such as qa and qd do when applied to qb.  If we do this just right, we
can prove a theorem saying that the ← can always be replaced by = in
a LISP definition, and we can use the resulting equation to prove properties
of the function.  (If we didn't do it right, the equation
for a LISP function would sometimes be
inconsistent, we would be able to prove anything, and no-one would believe
what we proved).